Nuprl Definition : ma-rframe
0,22
postcript
pdf
M
.rframe(
k
reads
x
)
==
L
!= 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(
M
)))))))))))(
x
)
deq-member(KindDeq;
k
;
L
)
latex
clarification:
M
.rframe(
k
reads
x
)
== fpf-val(IdDeq;
== fpf-val(
1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(
M
)))))))))));
== fpf-val(
x
;
== fpf-val(
x
,
L
.deq-member(KindDeq;
k
;
L
))
latex
Definitions
z
!=
f
(
x
)
P
(
a
;
z
)
,
IdDeq
,
1of(
t
)
,
2of(
t
)
,
b
,
deq-member(
eq
;
x
;
L
)
,
KindDeq
FDL editor aliases
ma-rframe
origin